/* Alloy Analyzer 4 -- Copyright (c) 2006-2009, Felix Chang
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files
 * (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify,
 * merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
 * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF
 * OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 */

package edu.mit.csail.sdg.alloy4;

/** This class receives diagnostic, progress, and warning messages from Alloy4.
 * (This default implementation ignores all calls; you should subclass it to do the appropriate screen output)
 */

public class A4Reporter {

   /** If nonnull, then we will forward requests to this reporter. */
   private final A4Reporter parent;

   /** This is a pre-constructed instance that simply ignores all calls. */
   public static final A4Reporter NOP = new A4Reporter();

   /** Constructs a default A4Reporter object that does nothing. */
   public A4Reporter () {
      parent = null;
   }

   /** Constructs an A4Reporter that forwards each method to the given A4Reporter. */
   public A4Reporter (A4Reporter reporter) {
      parent = reporter;
   }

   /** This method is called at various points to report the current progress;
    * it is intended as a debugging aid for the developers; the messages are generally not useful for end users.
    */
   public void debug (String msg) {
      if (parent != null) parent.debug(msg);
   }

   /** This method is called by the parser to report parser events. */
   public void parse (String msg) {
      if (parent != null) parent.parse(msg);
   }

   /** This method is called by the typechecker to report the type for each field/function/predicate/assertion, etc. */
   public void typecheck (String msg) {
      if (parent != null) parent.typecheck(msg);
   }

   /** This method is called by the typechecker to report a nonfatal type error. */
   public void warning (ErrorWarning msg) {
      if (parent != null) parent.warning(msg);
   }

   /** This method is called by the ScopeComputer to report the scope chosen for each sig. */
   public void scope (String msg) {
      if (parent != null) parent.scope(msg);
   }

   /** This method is called by the BoundsComputer to report the bounds chosen for each sig and each field. */
   public void bound (String msg) {
      if (parent != null) parent.bound(msg);
   }

   /** This method is called by the translator just before it begins generating CNF.
    *
    * @param solver - the solver chosen by the user (eg. SAT4J, MiniSat...)
    * @param bitwidth - the integer bitwidth chosen by the user
    * @param maxseq - the scope on seq/Int chosen by the user
    * @param skolemDepth - the skolem function depth chosen by the user (0, 1, 2...)
    * @param symmetry - the amount of symmetry breaking chosen by the user (0...)
    */
   public void translate (String solver, int bitwidth, int maxseq, int skolemDepth, int symmetry) {
      if (parent != null) parent.translate(solver, bitwidth, maxseq, skolemDepth, symmetry);
   }

   /** This method is called by the translator just after it generated the CNF.
    *
    * @param primaryVars - the total number of primary variables
    * @param totalVars - the total number of variables including the number of primary variables
    * @param clauses - the total number of clauses
    */
   public void solve (int primaryVars, int totalVars, int clauses) {
      if (parent != null) parent.solve(primaryVars, totalVars, clauses);
   }

   /** If solver==KK or solver==CNF, this method is called by the translator after it constructed the Kodkod or CNF file.
    *
    * @param filename - the Kodkod or CNF file generated by the translator
    */
   public void resultCNF (String filename) {
      if (parent != null) parent.resultCNF(filename);
   }

   /** If solver!=KK and solver!=CNF, this method is called by the translator if the formula is satisfiable.
    *
    * @param command - this is the original Command used to generate this solution
    * @param solvingTime - this is the number of milliseconds the solver took to obtain this result
    * @param solution - the satisfying A4Solution object
    */
   public void resultSAT (Object command, long solvingTime, Object solution) {
      if (parent != null) parent.resultSAT(command, solvingTime, solution);
   }

   /** If solver!=KK and solver!=CNF, this method is called by the translator before starting the unsat core minimization.
    *
    * @param command - this is the original Command used to generate this solution
    * @param before - the size of the unsat core before calling minimization
    */
   public void minimizing (Object command, int before) {
      if (parent != null) parent.minimizing(command, before);
   }

   /** If solver!=KK and solver!=CNF, this method is called by the translator after performing the unsat core minimization.
    *
    * @param command - this is the original Command used to generate this solution
    * @param before - the size of the unsat core before calling minimization
    * @param after - the size of the unsat core after calling minimization
    */
   public void minimized (Object command, int before, int after) {
      if (parent != null) parent.minimized(command, before, after);
   }

   /** If solver!=KK and solver!=CNF, this method is called by the translator if the formula is unsatisfiable.
    *
    * @param command - this is the original Command used to generate this solution
    * @param solvingTime - this is the number of milliseconds the solver took to obtain this result
    * @param solution - the unsatisfying A4Solution object
    */
   public void resultUNSAT (Object command, long solvingTime, Object solution) {
      if (parent != null) parent.resultUNSAT(command, solvingTime, solution);
   }

   /** This method is called by the A4SolutionWriter when it is writing a particular sig, field, or skolem. */
   public void write (Object expr) {
      if (parent != null) parent.write(expr);
   }
}
